Nuprl Definition : alle-at1
11,40
postcript
pdf
@
i
always.
P
(
x
) ==
e
@
i
.
P
(
x
when
e
)
latex
clarification:
alle-at1(
es
;
i
;
x
;
x
.
P
(
x
)) == alle-at(
es
;
i
;
e
.
P
(es-when(
es
;
x
;
e
)))
latex
Definitions
e
@
i
.
P
(
e
)
,
x
when
e
FDL editor aliases
alle-at1
origin
e@i. P(x when e)
e@i. P(x when e)
e@i. P(e)